@$i$ $x$ initially $v$:$T$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$vartype($i$;$x$) $\subseteq\rho$ $T$ \& $x$ initially@$i$  $=$ $v$